Nuprl Lemma : sframe-p-realizable
11,40
postcript
pdf
l
:IdLnk,
tg
:Id,
L
:(Knd List).
es
.only events in
L
send on
l
with
tg
latex
Definitions
x
.
t
(
x
)
,
,
t
T
,
x
:
A
.
B
(
x
)
,
es
.
P
(
es
)
,
x
:
A
.
B
(
x
)
,
x
(
s
)
Lemmas
IdLnk
wf
,
Id
wf
,
Knd
wf
,
event
system
wf
,
sframe-p
wf
,
R-realizes
wf
,
R-sframe-rule
,
Rsframe
wf
origin
l:IdLnk, tg:Id, L:(Knd List). 
es.only events in L send on l with tg l:IdLnk, tg:Id, L:(Knd List). es.only events in L send on l with tg 
x. t(x)
T
x:A. B(x)es.P(es)x:A. B(x)